--- All checks are done! No counterexample has been found!

in qlock .
---> 1
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p2 | p3) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 2
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p2 | p4) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 3
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p2 | p5) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 4
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p2 | p6) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 5
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p2 | p7) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 6
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p2 | p8) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 7
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p2 | p9) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 8
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p2 | p10) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 9
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p3 | p2) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 10
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p3 | p4) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 11
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p3 | p5) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 12
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p3 | p6) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 13
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p3 | p7) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 14
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p3 | p8) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 15
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p3 | p9) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 16
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p3 | p10) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 17
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p4 | p2) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 18
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p4 | p3) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 19
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p4 | p5) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 20
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p4 | p6) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 21
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p4 | p7) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 22
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p4 | p8) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 23
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p4 | p9) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 24
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p4 | p10) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 25
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p5 | p2) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 26
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p5 | p3) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 27
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p5 | p4) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 28
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p5 | p6) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 29
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p5 | p7) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 30
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p5 | p8) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 31
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p5 | p9) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 32
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p5 | p10) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 33
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p6 | p2) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 34
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p6 | p3) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 35
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p6 | p4) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 36
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p6 | p5) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 37
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p6 | p7) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 38
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p6 | p8) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 39
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p6 | p9) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 40
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p6 | p10) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 41
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p7 | p2) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 43
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p7 | p3) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 44
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p7 | p4) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 45
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p7 | p5) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 46
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p7 | p6) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 47
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p7 | p8) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 48
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p7 | p9) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 49
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p7 | p10) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 50
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p8 | p2) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 51
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p8 | p3) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 52
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p8 | p4) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 53
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p8 | p5) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 54
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p8 | p6) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 55
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p8 | p7) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 56
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p8 | p9) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 57
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p8 | p10) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 58
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p9 | p2) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 59
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p9 | p3) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 60
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p9 | p4) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 61
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p9 | p5) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 62
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p9 | p6) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 63
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p9 | p7) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 64
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p9 | p8) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 65
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p9 | p10) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ws}, <> inCs1) .
---> 66
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p10 | p2) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 67
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p10 | p3) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 68
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p10 | p4) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 69
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p10 | p5) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 70
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p10 | p6) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 71
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p10 | p7) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 72
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p10 | p8) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 73
  red in QLOCK-CHECK : modelCheck({queue: (p1 | p10 | p9) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ws}, <> inCs1) .
---> 74
  red in QLOCK-CHECK : modelCheck({queue: (p2 | p1 | p3) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 75
  red in QLOCK-CHECK : modelCheck({queue: (p2 | p1 | p4) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 76
  red in QLOCK-CHECK : modelCheck({queue: (p2 | p1 | p5) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 77
  red in QLOCK-CHECK : modelCheck({queue: (p2 | p1 | p6) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 78
  red in QLOCK-CHECK : modelCheck({queue: (p2 | p1 | p7) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 79
  red in QLOCK-CHECK : modelCheck({queue: (p2 | p1 | p8) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 80
  red in QLOCK-CHECK : modelCheck({queue: (p2 | p1 | p9) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 81
  red in QLOCK-CHECK : modelCheck({queue: (p2 | p1 | p10) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 82
  red in QLOCK-CHECK : modelCheck({queue: (p2 | p1) cnt: 10  (pc[p1]: ws) (
    pc[p2]: cs) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 83
  red in QLOCK-CHECK : modelCheck({queue: (p2 | p3 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 84
  red in QLOCK-CHECK : modelCheck({queue: (p2 | p4 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 85
  red in QLOCK-CHECK : modelCheck({queue: (p2 | p5 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 86
  red in QLOCK-CHECK : modelCheck({queue: (p2 | p6 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 87
  red in QLOCK-CHECK : modelCheck({queue: (p2 | p7 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 88
  red in QLOCK-CHECK : modelCheck({queue: (p2 | p8 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 89
  red in QLOCK-CHECK : modelCheck({queue: (p2 | p9 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 90
  red in QLOCK-CHECK : modelCheck({queue: (p2 | p10 | p1) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 91
  red in QLOCK-CHECK : modelCheck({queue: (p3 | p1 | p2) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 92
  red in QLOCK-CHECK : modelCheck({queue: (p3 | p1 | p4) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 93
  red in QLOCK-CHECK : modelCheck({queue: (p3 | p1 | p5) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 94
  red in QLOCK-CHECK : modelCheck({queue: (p3 | p1 | p6) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 95
  red in QLOCK-CHECK : modelCheck({queue: (p3 | p1 | p7) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 96
  red in QLOCK-CHECK : modelCheck({queue: (p3 | p1 | p8) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 97
  red in QLOCK-CHECK : modelCheck({queue: (p3 | p1 | p9) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 98
  red in QLOCK-CHECK : modelCheck({queue: (p3 | p1 | p10) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 99
  red in QLOCK-CHECK : modelCheck({queue: (p3 | p1) cnt: 10  (pc[p1]: ws) (
    pc[p2]: ss) (pc[p3]: cs) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 100
  red in QLOCK-CHECK : modelCheck({queue: (p3 | p2 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 101
  red in QLOCK-CHECK : modelCheck({queue: (p3 | p4 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 102
  red in QLOCK-CHECK : modelCheck({queue: (p3 | p5 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 103
  red in QLOCK-CHECK : modelCheck({queue: (p3 | p6 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 104
  red in QLOCK-CHECK : modelCheck({queue: (p3 | p7 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 105
  red in QLOCK-CHECK : modelCheck({queue: (p3 | p8 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 106
  red in QLOCK-CHECK : modelCheck({queue: (p3 | p9 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 107
  red in QLOCK-CHECK : modelCheck({queue: (p3 | p10 | p1) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 108
  red in QLOCK-CHECK : modelCheck({queue: (p4 | p1 | p2) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 109
  red in QLOCK-CHECK : modelCheck({queue: (p4 | p1 | p3) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 110
  red in QLOCK-CHECK : modelCheck({queue: (p4 | p1 | p5) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 111
  red in QLOCK-CHECK : modelCheck({queue: (p4 | p1 | p6) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 112
  red in QLOCK-CHECK : modelCheck({queue: (p4 | p1 | p7) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 113
  red in QLOCK-CHECK : modelCheck({queue: (p4 | p1 | p8) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 114
  red in QLOCK-CHECK : modelCheck({queue: (p4 | p1 | p9) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 115
  red in QLOCK-CHECK : modelCheck({queue: (p4 | p1 | p10) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 116
  red in QLOCK-CHECK : modelCheck({queue: (p4 | p1) cnt: 10  (pc[p1]: ws) (
    pc[p2]: ss) (pc[p3]: ss) (pc[p4]: cs) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 117
  red in QLOCK-CHECK : modelCheck({queue: (p4 | p2 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 118
  red in QLOCK-CHECK : modelCheck({queue: (p4 | p3 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 119
  red in QLOCK-CHECK : modelCheck({queue: (p4 | p5 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 120
  red in QLOCK-CHECK : modelCheck({queue: (p4 | p6 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 121
  red in QLOCK-CHECK : modelCheck({queue: (p4 | p7 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 122
  red in QLOCK-CHECK : modelCheck({queue: (p4 | p8 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 123
  red in QLOCK-CHECK : modelCheck({queue: (p4 | p9 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 124
  red in QLOCK-CHECK : modelCheck({queue: (p4 | p10 | p1) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 125
  red in QLOCK-CHECK : modelCheck({queue: (p5 | p1 | p2) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 126
  red in QLOCK-CHECK : modelCheck({queue: (p5 | p1 | p3) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 127
  red in QLOCK-CHECK : modelCheck({queue: (p5 | p1 | p4) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 128
  red in QLOCK-CHECK : modelCheck({queue: (p5 | p1 | p6) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 129
  red in QLOCK-CHECK : modelCheck({queue: (p5 | p1 | p7) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 130
  red in QLOCK-CHECK : modelCheck({queue: (p5 | p1 | p8) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 131
  red in QLOCK-CHECK : modelCheck({queue: (p5 | p1 | p9) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 132
  red in QLOCK-CHECK : modelCheck({queue: (p5 | p1 | p10) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 133
  red in QLOCK-CHECK : modelCheck({queue: (p5 | p1) cnt: 10  (pc[p1]: ws) (
    pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: cs) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 134
  red in QLOCK-CHECK : modelCheck({queue: (p5 | p2 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 135
  red in QLOCK-CHECK : modelCheck({queue: (p5 | p3 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 136
  red in QLOCK-CHECK : modelCheck({queue: (p5 | p4 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 137
  red in QLOCK-CHECK : modelCheck({queue: (p5 | p6 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 138
  red in QLOCK-CHECK : modelCheck({queue: (p5 | p7 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 139
  red in QLOCK-CHECK : modelCheck({queue: (p5 | p8 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 140
  red in QLOCK-CHECK : modelCheck({queue: (p5 | p9 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 142
  red in QLOCK-CHECK : modelCheck({queue: (p5 | p10 | p1) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 143
  red in QLOCK-CHECK : modelCheck({queue: (p6 | p1 | p2) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 144
  red in QLOCK-CHECK : modelCheck({queue: (p6 | p1 | p3) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 145
  red in QLOCK-CHECK : modelCheck({queue: (p6 | p1 | p4) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 146
  red in QLOCK-CHECK : modelCheck({queue: (p6 | p1 | p5) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 147
  red in QLOCK-CHECK : modelCheck({queue: (p6 | p1 | p7) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 148
  red in QLOCK-CHECK : modelCheck({queue: (p6 | p1 | p8) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 149
  red in QLOCK-CHECK : modelCheck({queue: (p6 | p1 | p9) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 150
  red in QLOCK-CHECK : modelCheck({queue: (p6 | p1 | p10) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 151
  red in QLOCK-CHECK : modelCheck({queue: (p6 | p1) cnt: 10  (pc[p1]: ws) (
    pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: cs) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 152
  red in QLOCK-CHECK : modelCheck({queue: (p6 | p2 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 153
  red in QLOCK-CHECK : modelCheck({queue: (p6 | p3 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 154
  red in QLOCK-CHECK : modelCheck({queue: (p6 | p4 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 155
  red in QLOCK-CHECK : modelCheck({queue: (p6 | p5 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 156
  red in QLOCK-CHECK : modelCheck({queue: (p6 | p7 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 157
  red in QLOCK-CHECK : modelCheck({queue: (p6 | p8 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 158
  red in QLOCK-CHECK : modelCheck({queue: (p6 | p9 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 159
  red in QLOCK-CHECK : modelCheck({queue: (p6 | p10 | p1) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 160
  red in QLOCK-CHECK : modelCheck({queue: (p7 | p1 | p2) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 161
  red in QLOCK-CHECK : modelCheck({queue: (p7 | p1 | p3) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 162
  red in QLOCK-CHECK : modelCheck({queue: (p7 | p1 | p4) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 163
  red in QLOCK-CHECK : modelCheck({queue: (p7 | p1 | p5) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 164
  red in QLOCK-CHECK : modelCheck({queue: (p7 | p1 | p6) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 165
  red in QLOCK-CHECK : modelCheck({queue: (p7 | p1 | p8) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 166
  red in QLOCK-CHECK : modelCheck({queue: (p7 | p1 | p9) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 167
  red in QLOCK-CHECK : modelCheck({queue: (p7 | p1 | p10) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 168
  red in QLOCK-CHECK : modelCheck({queue: (p7 | p1) cnt: 10  (pc[p1]: ws) (
    pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    cs) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 169
  red in QLOCK-CHECK : modelCheck({queue: (p7 | p2 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 170
  red in QLOCK-CHECK : modelCheck({queue: (p7 | p3 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 171
  red in QLOCK-CHECK : modelCheck({queue: (p7 | p4 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 172
  red in QLOCK-CHECK : modelCheck({queue: (p7 | p5 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 173
  red in QLOCK-CHECK : modelCheck({queue: (p7 | p6 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 174
  red in QLOCK-CHECK : modelCheck({queue: (p7 | p8 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 175
  red in QLOCK-CHECK : modelCheck({queue: (p7 | p9 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 176
  red in QLOCK-CHECK : modelCheck({queue: (p7 | p10 | p1) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 177
  red in QLOCK-CHECK : modelCheck({queue: (p8 | p1 | p2) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 178
  red in QLOCK-CHECK : modelCheck({queue: (p8 | p1 | p3) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 179
  red in QLOCK-CHECK : modelCheck({queue: (p8 | p1 | p4) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 180
  red in QLOCK-CHECK : modelCheck({queue: (p8 | p1 | p5) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 181
  red in QLOCK-CHECK : modelCheck({queue: (p8 | p1 | p6) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 182
  red in QLOCK-CHECK : modelCheck({queue: (p8 | p1 | p7) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 183
  red in QLOCK-CHECK : modelCheck({queue: (p8 | p1 | p9) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 184
  red in QLOCK-CHECK : modelCheck({queue: (p8 | p1 | p10) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 185
  red in QLOCK-CHECK : modelCheck({queue: (p8 | p1) cnt: 10  (pc[p1]: ws) (
    pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: cs) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 186
  red in QLOCK-CHECK : modelCheck({queue: (p8 | p2 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 187
  red in QLOCK-CHECK : modelCheck({queue: (p8 | p3 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 188
  red in QLOCK-CHECK : modelCheck({queue: (p8 | p4 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 189
  red in QLOCK-CHECK : modelCheck({queue: (p8 | p5 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 190
  red in QLOCK-CHECK : modelCheck({queue: (p8 | p6 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 191
  red in QLOCK-CHECK : modelCheck({queue: (p8 | p7 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
---> 192
  red in QLOCK-CHECK : modelCheck({queue: (p8 | p9 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 193
  red in QLOCK-CHECK : modelCheck({queue: (p8 | p10 | p1) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 194
  red in QLOCK-CHECK : modelCheck({queue: (p9 | p1 | p2) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 195
  red in QLOCK-CHECK : modelCheck({queue: (p9 | p1 | p3) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 196
  red in QLOCK-CHECK : modelCheck({queue: (p9 | p1 | p4) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 197
  red in QLOCK-CHECK : modelCheck({queue: (p9 | p1 | p5) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 198
  red in QLOCK-CHECK : modelCheck({queue: (p9 | p1 | p6) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 199
  red in QLOCK-CHECK : modelCheck({queue: (p9 | p1 | p7) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 200
  red in QLOCK-CHECK : modelCheck({queue: (p9 | p1 | p8) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 201
  red in QLOCK-CHECK : modelCheck({queue: (p9 | p1 | p10) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ws}, <> inCs1) .
---> 202
  red in QLOCK-CHECK : modelCheck({queue: (p9 | p1) cnt: 10  (pc[p1]: ws) (
    pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: cs) pc[p10]: ss}, <> inCs1) .
---> 203
  red in QLOCK-CHECK : modelCheck({queue: (p9 | p2 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 204
  red in QLOCK-CHECK : modelCheck({queue: (p9 | p3 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 205
  red in QLOCK-CHECK : modelCheck({queue: (p9 | p4 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 206
  red in QLOCK-CHECK : modelCheck({queue: (p9 | p5 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 207
  red in QLOCK-CHECK : modelCheck({queue: (p9 | p6 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[
    p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 208
  red in QLOCK-CHECK : modelCheck({queue: (p9 | p7 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ws) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 209
  red in QLOCK-CHECK : modelCheck({queue: (p9 | p8 | p1) cnt: 10  (pc[p1]:
    ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[
    p7]: ss) (pc[p8]: ws) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
---> 210
  red in QLOCK-CHECK : modelCheck({queue: (p9 | p10 | p1) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ws}, <> inCs1) .
---> 211
  red in QLOCK-CHECK : modelCheck({queue: (p10 | p1 | p2) cnt: 10 
    (pc[p1]: ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]:
    ss) (pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 212
  red in QLOCK-CHECK : modelCheck({queue: (p10 | p1 | p3) cnt: 10 
    (pc[p1]: ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]:
    ss) (pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 213
  red in QLOCK-CHECK : modelCheck({queue: (p10 | p1 | p4) cnt: 10 
    (pc[p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]:
    ss) (pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 214
  red in QLOCK-CHECK : modelCheck({queue: (p10 | p1 | p5) cnt: 10 
    (pc[p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]:
    ss) (pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 215
  red in QLOCK-CHECK : modelCheck({queue: (p10 | p1 | p6) cnt: 10 
    (pc[p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]:
    ws) (pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 216
  red in QLOCK-CHECK : modelCheck({queue: (p10 | p1 | p7) cnt: 10 
    (pc[p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]:
    ss) (pc[p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 217
  red in QLOCK-CHECK : modelCheck({queue: (p10 | p1 | p8) cnt: 10 
    (pc[p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]:
    ss) (pc[p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 218
  red in QLOCK-CHECK : modelCheck({queue: (p10 | p1 | p9) cnt: 10 
    (pc[p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]:
    ss) (pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ws}, <> inCs1) .
---> 219
  red in QLOCK-CHECK : modelCheck({queue: (p10 | p1) cnt: 10  (pc[
    p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (
    pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: cs}, <> inCs1) .
---> 220
  red in QLOCK-CHECK : modelCheck({queue: (p10 | p2 | p1) cnt: 10 
    (pc[p1]: ws) (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]:
    ss) (pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 221
  red in QLOCK-CHECK : modelCheck({queue: (p10 | p3 | p1) cnt: 10 
    (pc[p1]: ws) (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]:
    ss) (pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 222
  red in QLOCK-CHECK : modelCheck({queue: (p10 | p4 | p1) cnt: 10 
    (pc[p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]:
    ss) (pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 223
  red in QLOCK-CHECK : modelCheck({queue: (p10 | p5 | p1) cnt: 10 
    (pc[p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]:
    ss) (pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 224
  red in QLOCK-CHECK : modelCheck({queue: (p10 | p6 | p1) cnt: 10 
    (pc[p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]:
    ws) (pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 225
  red in QLOCK-CHECK : modelCheck({queue: (p10 | p7 | p1) cnt: 10 
    (pc[p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]:
    ss) (pc[p7]: ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 226
  red in QLOCK-CHECK : modelCheck({queue: (p10 | p8 | p1) cnt: 10 
    (pc[p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]:
    ss) (pc[p7]: ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
---> 227
  red in QLOCK-CHECK : modelCheck({queue: (p10 | p9 | p1) cnt: 10 
    (pc[p1]: ws) (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]:
    ss) (pc[p7]: ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ws}, <> inCs1) .

---> The results
==========================================
---> 1
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p2 | p3) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (765ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 2
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p2 | p4) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (671ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 3
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p2 | p5) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (681ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 4
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p2 | p6) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (686ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 5
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p2 | p7) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (697ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 6
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p2 | p8) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (684ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 7
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p2 | p9) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (691ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 8
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p2 | p10) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (690ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 9
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p3 | p2) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (694ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 10
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p3 | p4) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (687ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 11
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p3 | p5) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (680ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 12
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p3 | p6) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (675ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 13
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p3 | p7) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (691ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 14
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p3 | p8) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (688ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 15
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p3 | p9) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (679ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 16
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p3 | p10) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (676ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 17
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p4 | p2) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (698ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 18
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p4 | p3) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (689ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 19
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p4 | p5) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (682ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 20
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p4 | p6) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (674ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 21
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p4 | p7) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (688ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 22
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p4 | p8) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (689ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 23
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p4 | p9) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (678ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 24
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p4 | p10) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (673ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 25
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p5 | p2) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (692ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 26
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p5 | p3) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (689ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 27
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p5 | p4) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (678ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 28
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p5 | p6) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (676ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 29
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p5 | p7) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (691ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 30
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p5 | p8) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (686ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 31
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p5 | p9) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (679ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 32
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p5 | p10) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (676ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 33
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p6 | p2) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (690ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 34
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p6 | p3) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (692ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 35
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p6 | p4) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (677ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 36
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p6 | p5) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (731ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 37
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p6 | p7) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (617ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 38
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p6 | p8) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (682ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 39
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p6 | p9) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (674ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 40
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p6 | p10) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (678ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 41
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p7 | p2) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (691ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 43
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p7 | p3) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (692ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 44
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p7 | p4) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (693ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 45
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p7 | p5) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (677ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 46
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p7 | p6) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (692ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 47
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p7 | p8) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (685ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 48
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p7 | p9) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (679ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 49
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p7 | p10) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (689ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 50
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p8 | p2) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (689ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 51
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p8 | p3) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (688ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 52
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p8 | p4) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (681ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 53
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p8 | p5) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (675ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 54
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p8 | p6) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (692ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 55
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p8 | p7) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (688ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 56
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p8 | p9) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (681ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 57
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p8 | p10) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (677ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 58
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p9 | p2) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (697ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 59
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p9 | p3) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (689ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 60
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p9 | p4) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (679ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 61
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p9 | p5) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (680ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 62
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p9 | p6) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (693ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 63
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p9 | p7) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (685ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 64
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p9 | p8) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (681ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 65
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p9 | p10) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ws}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (678ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 66
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p10 | p2) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (690ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 67
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p10 | p3) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (690ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 68
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p10 | p4) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (679ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 69
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p10 | p5) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (673ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 70
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p10 | p6) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (692ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 71
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p10 | p7) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (691ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 72
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p10 | p8) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (679ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 73
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p1 | p10 | p9) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ws}, <> inCs1) .
rewrites: 54805 in 4332565049ms cpu (677ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 74
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p2 | p1 | p3) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (2151ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 75
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p2 | p1 | p4) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (2323ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 76
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p2 | p1 | p5) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (2349ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 77
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p2 | p1 | p6) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (2361ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 78
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p2 | p1 | p7) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (2359ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 79
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p2 | p1 | p8) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (2360ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 80
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p2 | p1 | p9) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (2366ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 81
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p2 | p1 | p10) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (2359ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 82
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p2 | p1) cnt: 10 (pc[p1]: ws) (pc[
    p2]: cs) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]: ss) (
    pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 986413 in 4332565049ms cpu (16686ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 83
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p2 | p3 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (5307ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 84
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p2 | p4 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (6913ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 85
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p2 | p5 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (7322ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 86
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p2 | p6 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8205ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 87
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p2 | p7 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8104ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 88
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p2 | p8 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (7985ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 89
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p2 | p9 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (6866ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 90
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p2 | p10 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8517ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 91
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p3 | p1 | p2) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5309ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 92
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p3 | p1 | p4) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5257ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 93
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p3 | p1 | p5) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (3680ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 94
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p3 | p1 | p6) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4377ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 95
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p3 | p1 | p7) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5078ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 96
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p3 | p1 | p8) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4963ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 97
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p3 | p1 | p9) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (3859ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 98
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p3 | p1 | p10) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4466ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 99
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p3 | p1) cnt: 10 (pc[p1]: ws) (pc[
    p2]: ss) (pc[p3]: cs) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]: ss) (
    pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 986413 in 4332565049ms cpu (30033ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 100
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p3 | p2 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (5934ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 101
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p3 | p4 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8595ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 102
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p3 | p5 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (7344ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 103
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p3 | p6 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8166ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 104
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p3 | p7 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (7997ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 105
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p3 | p8 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (7117ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 106
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p3 | p9 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8536ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 107
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p3 | p10 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8273ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 108
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p4 | p1 | p2) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4804ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 109
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p4 | p1 | p3) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5134ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 110
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p4 | p1 | p5) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4883ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 111
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p4 | p1 | p6) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (3932ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 112
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p4 | p1 | p7) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4573ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 113
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p4 | p1 | p8) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5289ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 114
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p4 | p1 | p9) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4649ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 115
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p4 | p1 | p10) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4083ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 116
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p4 | p1) cnt: 10 (pc[p1]: ws) (pc[
    p2]: ss) (pc[p3]: ss) (pc[p4]: cs) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]: ss) (
    pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 986413 in 4332565049ms cpu (30290ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 117
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p4 | p2 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (6089ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 118
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p4 | p3 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8576ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 119
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p4 | p5 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (7261ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 120
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p4 | p6 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8160ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 121
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p4 | p7 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (7932ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 122
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p4 | p8 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (7063ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 123
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p4 | p9 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8505ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 124
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p4 | p10 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8351ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 125
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p5 | p1 | p2) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5056ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 126
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p5 | p1 | p3) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5597ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 127
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p5 | p1 | p4) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4807ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 128
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p5 | p1 | p6) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (3765ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 129
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p5 | p1 | p7) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4538ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 130
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p5 | p1 | p8) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5186ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 131
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p5 | p1 | p9) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4773ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 132
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p5 | p1 | p10) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4076ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 133
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p5 | p1) cnt: 10 (pc[p1]: ws) (pc[
    p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: cs) (pc[p6]: ss) (pc[p7]: ss) (
    pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 986413 in 4332565049ms cpu (30426ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 134
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p5 | p2 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (6174ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 135
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p5 | p3 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8586ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 136
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p5 | p4 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (7333ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 137
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p5 | p6 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8140ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 138
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p5 | p7 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (7973ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 139
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p5 | p8 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (6966ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 140
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p5 | p9 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8589ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 142
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p5 | p10 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8310ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 143
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p6 | p1 | p2) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4741ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 144
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p6 | p1 | p3) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5030ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 145
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p6 | p1 | p4) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5029ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 146
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p6 | p1 | p5) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (3787ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 147
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p6 | p1 | p7) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4423ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 148
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p6 | p1 | p8) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5083ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 149
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p6 | p1 | p9) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4923ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 150
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p6 | p1 | p10) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (3821ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 151
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p6 | p1) cnt: 10 (pc[p1]: ws) (pc[
    p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: cs) (pc[p7]: ss) (
    pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 986413 in 4332565049ms cpu (31503ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 152
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p6 | p2 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (5156ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 153
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p6 | p3 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (6542ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 154
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p6 | p4 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8033ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 155
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p6 | p5 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (7964ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 156
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p6 | p7 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (7415ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 157
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p6 | p8 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8930ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 158
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p6 | p9 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8094ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 159
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p6 | p10 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8446ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 160
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p7 | p1 | p2) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5199ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 161
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p7 | p1 | p3) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5490ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 162
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p7 | p1 | p4) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (3588ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 163
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p7 | p1 | p5) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4650ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 164
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p7 | p1 | p6) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5553ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 165
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p7 | p1 | p8) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4564ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 166
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p7 | p1 | p9) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4539ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 167
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p7 | p1 | p10) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5212ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 168
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p7 | p1) cnt: 10 (pc[p1]: ws) (pc[
    p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]: cs) (
    pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 986413 in 4332565049ms cpu (33470ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 169
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p7 | p2 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (5175ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 170
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p7 | p3 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (6871ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 171
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p7 | p4 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8080ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 172
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p7 | p5 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (7997ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 173
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p7 | p6 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (7563ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 174
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p7 | p8 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8951ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 175
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p7 | p9 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8160ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 176
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p7 | p10 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8454ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 177
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p8 | p1 | p2) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5286ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 178
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p8 | p1 | p3) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5324ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 179
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p8 | p1 | p4) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (3696ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 180
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p8 | p1 | p5) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4717ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 181
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p8 | p1 | p6) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5527ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 182
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p8 | p1 | p7) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4509ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 183
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p8 | p1 | p9) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4542ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 184
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p8 | p1 | p10) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5184ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 185
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p8 | p1) cnt: 10 (pc[p1]: ws) (pc[
    p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]: ss) (
    pc[p8]: cs) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 986413 in 4332565049ms cpu (34624ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 186
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p8 | p2 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (5167ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 187
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p8 | p3 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (6944ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 188
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p8 | p4 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8060ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 189
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p8 | p5 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (7953ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 190
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p8 | p6 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (7507ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 191
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p8 | p7 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8924ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 192
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p8 | p9 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8072ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 193
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p8 | p10 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8514ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 194
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p9 | p1 | p2) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5265ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 195
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p9 | p1 | p3) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5392ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 196
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p9 | p1 | p4) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (3690ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 197
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p9 | p1 | p5) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4710ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 198
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p9 | p1 | p6) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5519ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 199
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p9 | p1 | p7) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4535ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 200
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p9 | p1 | p8) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4543ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 201
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p9 | p1 | p10) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ws}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5187ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 202
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p9 | p1) cnt: 10 (pc[p1]: ws) (pc[
    p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]: ss) (
    pc[p8]: ss) (pc[p9]: cs) pc[p10]: ss}, <> inCs1) .
rewrites: 986413 in 4332565049ms cpu (34577ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 203
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p9 | p2 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (5160ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 204
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p9 | p3 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (6916ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 205
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p9 | p4 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8053ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 206
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p9 | p5 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (7948ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 207
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p9 | p6 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (7519ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 208
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p9 | p7 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8938ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 209
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p9 | p8 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ws) pc[p10]: ss}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8072ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 210
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p9 | p10 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ws}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8457ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 211
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p10 | p1 | p2) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5269ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 212
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p10 | p1 | p3) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5376ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 213
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p10 | p1 | p4) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (3690ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 214
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p10 | p1 | p5) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4687ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 215
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p10 | p1 | p6) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5507ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 216
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p10 | p1 | p7) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4534ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 217
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p10 | p1 | p8) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (4592ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 218
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p10 | p1 | p9) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ws}, <> inCs1) .
rewrites: 164403 in 4332565049ms cpu (5195ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 219
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p10 | p1) cnt: 10 (pc[p1]: ws) (pc[
    p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]: ss) (
    pc[p8]: ss) (pc[p9]: ss) pc[p10]: cs}, <> inCs1) .
rewrites: 986413 in 4332565049ms cpu (34546ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 220
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p10 | p2 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ws) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (5174ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 221
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p10 | p3 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ws) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (6907ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 222
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p10 | p4 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ws) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8062ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 223
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p10 | p5 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ws) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (7952ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 224
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p10 | p6 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ws) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (7499ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 225
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p10 | p7 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ws) (pc[p8]: ss) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8917ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 226
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p10 | p8 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ws) (pc[p9]: ss) pc[p10]: ws}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8103ms real) (0 rewrites/second)
result Bool: true
==========================================
---> 227
==========================================
reduce in QLOCK-CHECK : modelCheck({queue: (p10 | p9 | p1) cnt: 10 (pc[p1]: ws)
    (pc[p2]: ss) (pc[p3]: ss) (pc[p4]: ss) (pc[p5]: ss) (pc[p6]: ss) (pc[p7]:
    ss) (pc[p8]: ss) (pc[p9]: ws) pc[p10]: ws}, <> inCs1) .
rewrites: 274001 in 4332565049ms cpu (8470ms real) (0 rewrites/second)
result Bool: true